\begin{tabbing}
$\forall$$P_{1}$:(es\_realizer\{i:l\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]$P_{1}$($\cdot$)
\\[0ex]$\Rightarrow$ ($\forall$${\it left}$, ${\it right}$:es\_realizer\{i:l\}. $P_{1}$(${\it left}$) $\Rightarrow$ $P_{1}$(${\it right}$) $\Rightarrow$ $P_{1}$(${\it left}$ $\oplus$ ${\it right}$))
\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$:Id, $T$:Type$_{\mbox{\scriptsize i}}$, $x$:Id, $v$:$T$. $P_{1}$(@${\it loc}$ $x$ initially $v$:$T$))
\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$:Id, $T$:Type$_{\mbox{\scriptsize i}}$, $x$:Id, $L$:Knd List. $P_{1}$(@${\it loc}$ only events in $L$ change $x$:$T$))
\\[0ex]$\Rightarrow$ ($\forall$${\it lnk}$:IdLnk, ${\it tag}$:Id, $L$:Knd List. $P_{1}$(only events in $L$ send on ${\it lnk}$ with ${\it tag}$))
\\[0ex]$\Rightarrow$ (\=$\forall$\=${\it loc}$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, ${\it knd}$:Knd, $T$:Type$_{\mbox{\scriptsize i}}$, $x$:Id,\+\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$decl{-}type\=\{i:l\}\+
\\[0ex](${\it ds}$; $x$)).
\-\-\\[0ex]$P_{1}$(@${\it loc}$ effect ${\it knd}$(v:$T$)  $x$ := $f$ State(${\it ds}$) v ))
\-\\[0ex]$\Rightarrow$ (\=$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, ${\it knd}$:Knd, $T$:Type$_{\mbox{\scriptsize i}}$, $l$:IdLnk, ${\it dt}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$,\+\+
\\[0ex]$g$:(${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$(decl{-}type\{i:l\}(${\it dt}$; ${\it tg}$) List))) List.
\-\\[0ex]$P_{1}$(sends ${\it knd}$(v:$T$) on $l$:tagged($g$,State(${\it ds}$),v):${\it dt}$))
\-\\[0ex]$\Rightarrow$ (\=$\forall$${\it loc}$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, $a$:Id, $T$:Type$_{\mbox{\scriptsize i}}$, $P$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$Prop$_{\mbox{\scriptsize i}}$).\+
\\[0ex]$P_{1}$(@${\it loc}$ precondition for $a$(v:$T$):$P$ State(${\it ds}$) v))
\-\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$:Id, $k$:Knd, $L$:Id List. $P_{1}$(@${\it loc}$: $k$ writes only members of $L$))
\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$:Id, $k$:Knd, $L$:IdLnk List. $P_{1}$(@${\it loc}$: $k$ sends only on links in $L$))
\\[0ex]$\Rightarrow$ ($\forall$${\it loc}$, $x$:Id, $L$:Knd List. $P_{1}$(@${\it loc}$: only members of $L$ read $x$))
\\[0ex]$\Rightarrow$ \{$\forall$$x_{1}$:es\_realizer\{i:l\}. $P_{1}$($x_{1}$)\}
\end{tabbing}